es:ES, i, x:Id, T:Type, I:(TProp).
vartype(i;x)  T & e@i. first(e)  I(x when e)
 e@i. I(x when e)  I((x after e))
 @i always.I(x) 

latex

Definitions	t  T, True, T, ES, Id, x:A. B(x), x(s), P  Q, P  Q, P & Q, P  Q, E, Prop, first(e), b, A, e@i. P(e), x. t(x), @i always.P(x), A & B, x when e, pred(e), (x after e), loc(e), vartype(i;x)
Lemmas	es-after wf, alle-at-iff, alle-at wf, not wf, assert wf, es-first wf, es-loc wf, es-E wf, es-pred wf, es-loc-pred, es-after-pred, es-when wf, subtype rel wf, es-vartype wf, squash wf, true wf, Id wf, event system wf